package controlGraph;

import java.util.ArrayList;
import java.util.HashMap;
import java.util.Iterator;
import java.util.List;
import java.util.Map;

/**
 * @author Administrator
 * This is Store element which will contain the actual concrete values which 
 * which will be used for the generation of the axioms and value manipulation
 */
public class store {
	
	/**
	 * This is the only element in the whole class. The function of the 
	 * class controls the whole map.
	 */
	private Map<String,StoreValue> map;
	
	public store(store source){
		Map<String,StoreValue> temp = source.getMap();
		
		if(temp == null){
			this.map = null;
		}
		else{
			this.map = new HashMap<String,StoreValue>(source.getMap());
		}
	}
	
	public store(){
		this.map = new HashMap<String,StoreValue>();
	}
	
	/**
	 * @param Variable
	 * @return Returns the Value of the Map map
	 */
	
	public Map<String, StoreValue> getMap(){
		return this.map;
	}
	
	/**
	 * @param Variable
	 * @return Returns the StoreValue for the corresponding Key
	 */
	public StoreValue getStoreValue(String Variable){
		return this.map.get(Variable);
	}
	
	/**
	 * Add variable to the sigma
	 * @param name - Variable name
	 * @param dimension - Dimension of the array
	 * @param expr - Corresponding Expression
	 */
	public void addVariable(String name, int reference, Expression expr){
		this.map.put(name, new StoreValue(reference, expr));
	}
	
	/**
	 * @param lhs
	 * @param rhs
	 *  Changes the zigma
	 */
	public void changeVariable(Expression lhs, Expression rhs) {
		//First we shall see if the rhs is perfect i.e. no array out of bounds
		Expression RHSLValue = getLValueInt(rhs);		
		
		//This below is replaced by the above code 
		
		/*if(rhs instanceof LValueInt){
			RHSLValue = new LValueInt((LValueInt)rhs);
		}
		
		if(rhs instanceof Variable){
			Variable temp = ((Variable)rhs);
			String VariName = temp.getVariable();
			StoreValue value = Statement.zigma.getStoreValue(VariName);
			Expression Right = value.getExpression();
			if(Right instanceof UndefinedExpression){
				RHSLValue = UndefinedExpression.getInstance();
			}
			else{
				RHSLValue = new LValueInt((LValueInt) (value.getExpression()));
			}
			
		}
		
		if(rhs instanceof ArrayRef){
			ArrayRef temp = (ArrayRef) rhs;
			String variable_name = temp.getVariable();
			Expression index = temp.getIndexExpression();
			
			//newly added code to handle Undefined
			StoreValue value = Statement.zigma.getStoreValue(variable_name);
			
			//Get the candidate ArrayExpression
			Expression Right = value.getExpression();
			if(!(Right instanceof UndefinedExpression)){
			ArrayList<String> empty = new ArrayList<String>();
			
			//Called SAT solver
			if(Statement.getResult(variable_name, index,empty )){
				
				//Check if a array
				if(!(Right instanceof ArrayLitExpression) ){
					System.out.println("Trying to array access a non-array");
				}
				
				//Determine the Index
				if(index instanceof Variable){
					index = new LValueInt(Statement.zigma.getLValueInt(index));
				}
				if(index instanceof LValueInt){
					//nothing to change
				}
				
				//Get the corresponding expression
				Expression resultant = ((ArrayLitExpression)Right).getExpressionAtIndex(((LValueInt)index).getValue());
				
				//Check if the RValue is undefined or defined to LValueInt
				if(resultant instanceof UndefinedExpression){
					RHSLValue = resultant;
				}
				if(resultant instanceof LValueInt){
					RHSLValue = new LValueInt(index);
				}
				
				RHSLValue = new LValueInt(index);
				System.out.println("The array access in "+variable_name+" is valid");
			}else{
				System.out.println("This array reference is Unsatisfiable");
				System.exit(1);
			}
			}//end-if
			else{
				RHSLValue = UndefinedExpression.getInstance();
			}
		}*/
		
		if(lhs instanceof LValueInt){
			System.out.println("RValue cannot be assigned . we need a LValue - Store<FILE> - Change Variable<Method>  ");
			System.exit(1);
			
		}
		
		if(lhs instanceof Variable){
			Variable temp = (Variable)lhs;
			String VariName = temp.getVariable();
			Statement.rules.removeArith(lhs); // Removes the related axioms
			this.map.put(VariName, new StoreValue(0, RHSLValue));			
		}
		
		if(lhs instanceof ArrayRef){
			ArrayRef temp = (ArrayRef) lhs;
			String variable_name = temp.getVariable();
			Expression index = temp.getIndexExpression();
			ArrayList<String> empty = new ArrayList<String>();
			
			if(Statement.getResult(variable_name, index, empty)){
				//get the LValue of the index
				Expression indexValue = getLValueInt(index);
				if(indexValue instanceof LValueInt){
					Expression shouldBeArray = Statement.zigma.getStoreValue(temp.getVariable()).getExpression();
					if(! (shouldBeArray instanceof ArrayLitExpression)){
						System.out.println("There is no array for this variable - File Store - Method getLValueInt(Expression rhs) ");
						System.exit(1);
					}
					
					//Get the array
					Expression ArrayLitExpr = this.map.get(variable_name).getExpression();
					if(!(ArrayLitExpr instanceof ArrayLitExpression)){
						System.out.println("!(ArrayLitExpr instanceof ArrayLitExpression) is False . It CANNOT BE !!!!");
						System.exit(1);
					}
					
					//Set the element in the array
					((ArrayLitExpression)ArrayLitExpr).setExpresionAtIndex(((LValueInt)indexValue).getValue(), RHSLValue);
					Statement.rules.removeArith(lhs);//Removes the related axioms
				}
				if(indexValue instanceof UndefinedExpression){
					//Ideally the whole array should be wiped to undefined value;
					//All the axioms pertaining to the each element should be wiped
				
					//Undefines all the values of the array
					int ArraySize = this.map.get(variable_name).getRef();
					ArrayList<Expression> tempArrayList = new ArrayList<Expression>();
					for(int j=0;j<ArraySize;++j){
						tempArrayList.add(UndefinedExpression.getInstance());
					}
					Expression[] arg= (Expression[])tempArrayList.toArray(new Expression[tempArrayList.size()]); 
					ArrayLitExpression tempArray = new ArrayLitExpression(arg);
					this.map.put(variable_name, new StoreValue(ArraySize,tempArray));
					
					// Removes axioms related to the whole array
					Statement.rules.removeArith(temp.getVariableExpression()); 
				}
			}//if-Statement.getResult()
		}
	}
	
	public Expression getLValueInt(Expression rhs){
		Expression RHSLValue = UndefinedExpression.getInstance();
		
		
		if(rhs instanceof LValueInt){
			RHSLValue = new LValueInt((LValueInt)rhs);
		}
		
		if(rhs instanceof Variable){
			Variable temp = ((Variable)rhs);
			String VariName = temp.getVariable();
			StoreValue value = Statement.zigma.getStoreValue(VariName);
			
			//If the variable is never declared !!!
			if(value == null){
				System.out.println("Compiler error: No Variable "+VariName+" defined");
				System.exit(1);
			}
			
			Expression e = value.getExpression();
			if(e instanceof UndefinedExpression){
				RHSLValue = UndefinedExpression.getInstance();
			}
			if(e instanceof LValueInt) {
				RHSLValue = new LValueInt((LValueInt) (e));
			}
			
			if(!((e instanceof LValueInt) || (e instanceof UndefinedExpression))){
				System.out.println("Error : The stored Expression for the variable "+VariName+"  doesn't have a LValueInt stored");
				System.exit(1);
			}
		}
		
		if(rhs instanceof ArrayRef){
			ArrayRef temp = (ArrayRef) rhs;
			String variable_name = temp.getVariable();
			Expression index = temp.getIndexExpression();
			ArrayList<String> empty = new ArrayList<String>();
			
			//Called SAT solver
			if(Statement.getResult(variable_name, index,empty )){
				Expression indexValue = getLValueInt(index);
				
				if(indexValue instanceof LValueInt){
					Expression shouldBeArray = Statement.zigma.getStoreValue(variable_name).getExpression();
					if(! (shouldBeArray instanceof ArrayLitExpression)){
						System.out.println("There is no array for this variable - File Store - Method getLValueInt(Expression rhs) ");
						System.exit(1);
					}
					return ((ArrayLitExpression)shouldBeArray).getExpressionAtIndex(((LValueInt)indexValue).getValue());
				}
				
				if(indexValue instanceof UndefinedExpression){
					return indexValue;
				}
			}
			else
			{
				System.out.println("This array reference is Unsatisfiable");
				System.exit(1);
			}
		}
		
		return RHSLValue;
	}
}
